Nuprl Lemma : Rlist-has-loc
11,40
postcript
pdf
L
:(top List),
i
:top.
sqequal(R-has-loc(Rlist(
L
);
i
); reduce((
A
,
b
. bor(R-has-loc(
A
;
i
);
b
)); ff;
L
))
latex
Definitions
t
T
,
Y
,
reduce(
f
;
k
;
as
)
,
Rlist(
L
)
,
R-has-loc(
R
;
i
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
L:(top List), i:top.
A,b. bor(R-has-loc(A; i); b)); ff; L)) L:(top List), i:top.
A,b. bor(R-has-loc(A; i); b)); ff; L)) 
Tx:A. B(x)